Add safety preconditions to alloc/src/alloc.rs #118
Conversation
These changes add code contracts in the form of `#[requires(...)]` attributes to various methods in the `Global` allocator implementation. These contracts ensure that the safety conditions mentioned in the comments are explicitly stated as preconditions for the functions.
Just as previously done for core: this will enable future use of
`safety::{ensures,requires}` in those crates.
|
How does one do contracts for traits? kani complains that it cannot find any of the contracts that have been added to functions in |
|
AFAIK, this is currently not supported: model-checking/kani#1997 We have a test that is disabled till support is added: https://github.com/model-checking/kani/blob/main/tests/expected/function-contract/trait_impls/methods.rs |
| #[requires(layout.size() == 0 || layout.align() != 0)] | ||
| #[requires(ptr.as_ptr() as usize % layout.align() == 0)] |
There was a problem hiding this comment.
don't we need to require that the pointer is actually allocated?
There was a problem hiding this comment.
We actually need an even stronger precondition (and Kani correctly detects this via the grow_impl harness): we'd need to express that ptr either points to a ZST (that's doable) or is a valid heap allocation (I don't know how we could currently express this).
Yes, see #118 (comment). |
These changes add code contracts in the form of
#[requires(...)]attributes to various methods in theGlobalallocator implementation. These contracts ensure that the safety conditions mentioned in the comments are explicitly stated as preconditions for the functions.